(set-logic BV)
(synth-fun f ( (x (BitVec 64)) ) (BitVec 64)
((Start (BitVec 64)
((bvnot Start)
(bvxor Start Start)
(bvand Start Start)
(bvor Start Start)
(bvneg Start)
(bvadd Start Start)
(bvmul Start Start)
(bvudiv Start Start)
(bvurem Start Start)
(bvlshr Start Start)
(bvashr Start Start)
(bvshl Start Start)
(bvsdiv Start Start)
(bvsrem Start Start)
(bvsub Start Start)
x
#x0000000000000000
#x0000000000000001
#x0000000000000002
#x0000000000000003
#x0000000000000004
#x0000000000000005
#x0000000000000006
#x0000000000000007
#x0000000000000008
#x0000000000000009
#x0000000000000009
#x0000000000000009
#x000000000000000A
#x000000000000000B
#x000000000000000C
#x000000000000000D
#x000000000000000E
#x000000000000000F
#x0000000000000010
(ite StartBool Start Start)
))
(StartBool Bool
((= Start Start)
(not StartBool)
(and StartBool StartBool)
(or StartBool StartBool)
))))
(constraint (= (f #x2e14b48ac339abed) #x5c296915867357da))
(constraint (= (f #x8cd06941e36e9910) #x732f96be1c9166ef))
(constraint (= (f #xbcc1e57687c895d3) #xbcc1e57687c895d3))
(constraint (= (f #x85e15e943b9562e0) #x7a1ea16bc46a9d1f))
(constraint (= (f #x8ea036e24cd8c3c4) #x715fc91db3273c3b))
(constraint (= (f #xc7e144aead6be4ab) #xc7e144aead6be4ab))
(constraint (= (f #x7cb963ae36e5bd4e) #x83469c51c91a42b1))
(constraint (= (f #x45c59977e6c129e4) #xba3a6688193ed61b))
(constraint (= (f #x6a879369140192c1) #x6a879369140192c1))
(constraint (= (f #x6ac339e36ebb0b87) #xd58673c6dd76170e))
(constraint (= (f #x58a488070482e5e4) #xa75b77f8fb7d1a1b))
(constraint (= (f #xe2d57d84be153075) #xc5aafb097c2a60ea))
(constraint (= (f #x97b4aae7906cce93) #x97b4aae7906cce93))
(constraint (= (f #xe9ae001db3e97d5d) #xe9ae001db3e97d5d))
(constraint (= (f #x3ee4c568b52e4d65) #x3ee4c568b52e4d65))
(constraint (= (f #x3d98e97693c344d2) #xc26716896c3cbb2d))
(constraint (= (f #xe43339d49e716665) #xc86673a93ce2ccca))
(constraint (= (f #x7d7cd090379ee058) #x82832f6fc8611fa7))
(constraint (= (f #x3d06a70dca42b679) #x3d06a70dca42b679))
(constraint (= (f #xbb741ea64263e69d) #xbb741ea64263e69d))
(constraint (= (f #x9a8edd52326daaee) #x657122adcd925511))
(constraint (= (f #xd4ac3a947be30979) #xd4ac3a947be30979))
(constraint (= (f #x12e9cae33e6ebb7a) #xed16351cc1914485))
(constraint (= (f #x812ed13324eeb738) #x7ed12eccdb1148c7))
(constraint (= (f #x8becc869a0e39bc0) #x741337965f1c643f))
(constraint (= (f #x9ae08eec1e81098d) #x9ae08eec1e81098d))
(constraint (= (f #x10da283e2388d08d) #x10da283e2388d08d))
(constraint (= (f #x0ee502e19b771d50) #xf11afd1e6488e2af))
(constraint (= (f #x16c3aad7b30a25cb) #x16c3aad7b30a25cb))
(constraint (= (f #xe30ec70ebcd49607) #xc61d8e1d79a92c0e))
(constraint (= (f #x82070ce195a074ee) #x7df8f31e6a5f8b11))
(constraint (= (f #x5bda1ce276993e54) #xa425e31d8966c1ab))
(constraint (= (f #xe46ee33406d35700) #x1b911ccbf92ca8ff))
(constraint (= (f #x4ea1dee825b9e2a5) #x9d43bdd04b73c54a))
(constraint (= (f #xecdade65ccb9b02c) #x1325219a33464fd3))
(constraint (= (f #x828a48864c72417a) #x7d75b779b38dbe85))
(constraint (= (f #x1dbc98396bc9c99d) #x1dbc98396bc9c99d))
(constraint (= (f #x791a09a6d1ac2dee) #x86e5f6592e53d211))
(constraint (= (f #xbd036a035d0b0611) #xbd036a035d0b0611))
(constraint (= (f #x55ee319d0870eeee) #xaa11ce62f78f1111))
(constraint (= (f #x3e9e3a4110dedc09) #x7d3c748221bdb812))
(constraint (= (f #x4e2e8dc2a1b4531b) #x9c5d1b854368a636))
(constraint (= (f #x5e8d9204a7299074) #xa1726dfb58d66f8b))
(constraint (= (f #x55322e40dcdca49e) #xaacdd1bf23235b61))
(constraint (= (f #x493d74e4517c61ad) #x927ae9c8a2f8c35a))
(constraint (= (f #x433e93bbe649b964) #xbcc16c4419b6469b))
(constraint (= (f #xc1ebda68e07e1910) #x3e1425971f81e6ef))
(constraint (= (f #x60d62d657427e695) #x60d62d657427e695))
(constraint (= (f #x06e9aebb8190e287) #x0dd35d770321c50e))
(constraint (= (f #x978044e05aec7867) #x978044e05aec7867))
(constraint (= (f #x5081604d36843e93) #x5081604d36843e93))
(constraint (= (f #xcd3e62006c6bbc48) #x32c19dff939443b7))
(constraint (= (f #x76a91be816c11329) #x76a91be816c11329))
(constraint (= (f #xa84c938626c5291d) #xa84c938626c5291d))
(constraint (= (f #x560c6e5deee8d278) #xa9f391a211172d87))
(constraint (= (f #xb79b2a25178dd25e) #x4864d5dae8722da1))
(constraint (= (f #x1dc31b872e34230e) #xe23ce478d1cbdcf1))
(constraint (= (f #xe0317e4e520a1c0d) #xe0317e4e520a1c0d))
(constraint (= (f #xc454c4e7d9150232) #x3bab3b1826eafdcd))
(constraint (= (f #x39b68ab24eb01423) #x736d15649d602846))
(constraint (= (f #xb0ebe51a053ab793) #x61d7ca340a756f26))
(constraint (= (f #xd88ae28965ecc026) #x27751d769a133fd9))
(constraint (= (f #xecea84eb4c15a22a) #x13157b14b3ea5dd5))
(constraint (= (f #xee42e2ba2993e413) #xdc85c5745327c826))
(constraint (= (f #x4d2429ece40775b7) #x4d2429ece40775b7))
(constraint (= (f #x78eb8a37aea9d558) #x871475c851562aa7))
(constraint (= (f #xad2c76cc5d5548bb) #x5a58ed98baaa9176))
(constraint (= (f #xb7cceb4c327ecee0) #x483314b3cd81311f))
(constraint (= (f #x85dbb4d600e7c426) #x7a244b29ff183bd9))
(constraint (= (f #xe38b9c9850d6d8be) #x1c746367af292741))
(constraint (= (f #xcb12ad33c97d7e51) #x96255a6792fafca2))
(constraint (= (f #xabaaab3acec912c4) #x545554c53136ed3b))
(constraint (= (f #xe356091b6219ea25) #xc6ac1236c433d44a))
(constraint (= (f #x8837ee6e5c9085a4) #x77c81191a36f7a5b))
(constraint (= (f #x6de660a75646e1cb) #x6de660a75646e1cb))
(constraint (= (f #x94183c60b93c77ec) #x6be7c39f46c38813))
(constraint (= (f #x0a865318d3c2a580) #xf579ace72c3d5a7f))
(constraint (= (f #x86029390db0de4e6) #x79fd6c6f24f21b19))
(constraint (= (f #x80126eb3bb17dc8e) #x7fed914c44e82371))
(constraint (= (f #xee87bee7e2132a47) #xdd0f7dcfc426548e))
(constraint (= (f #x2e2281ea237e01b4) #xd1dd7e15dc81fe4b))
(constraint (= (f #xe4ba7153b69825dc) #x1b458eac4967da23))
(constraint (= (f #xb4ac1e0ee6399dd9) #x69583c1dcc733bb2))
(constraint (= (f #x8e5b913a46dcb1ce) #x71a46ec5b9234e31))
(constraint (= (f #x5e15b7ee691a1455) #xbc2b6fdcd23428aa))
(constraint (= (f #x7986ad733112bb51) #xf30d5ae6622576a2))
(constraint (= (f #xe2dbcd571505e39c) #x1d2432a8eafa1c63))
(constraint (= (f #x6cba870920ceb54b) #x6cba870920ceb54b))
(constraint (= (f #x8a2eeb9dc13e59ee) #x75d114623ec1a611))
(constraint (= (f #x6c9e734e1b3617ee) #x93618cb1e4c9e811))
(constraint (= (f #xbd9545ccc370b481) #x7b2a8b9986e16902))
(constraint (= (f #x9de0ec6e7ede2cdb) #x3bc1d8dcfdbc59b6))
(constraint (= (f #x0b556de65e6e810d) #x0b556de65e6e810d))
(constraint (= (f #xd85d842de7b5e805) #xb0bb085bcf6bd00a))
(constraint (= (f #xab840a22d5a3494a) #x547bf5dd2a5cb6b5))
(constraint (= (f #x24ebcdae95b59970) #xdb1432516a4a668f))
(constraint (= (f #x56dc684223257d42) #xa92397bddcda82bd))
(constraint (= (f #x1664009ceebad062) #xe99bff6311452f9d))
(constraint (= (f #xec3136846c5e9dce) #x13cec97b93a16231))
(constraint (= (f #x23c85a196d128a97) #x4790b432da25152e))
(check-synth)
(define-fun f_1 ((x (BitVec 64))) (BitVec 64) (ite (= (bvand #x0000000000000001 x) #x0000000000000000) (bvnot x) (ite (= (bvor #x000000000000000c x) x) (ite (= (bvurem x #x0000000000000003) #x0000000000000001) x (ite (= (bvsrem x #x0000000000000007) #x0000000000000000) (bvadd x x) (ite (= (bvashr x x) #x0000000000000000) (ite (= (bvand #x0000000000000010 x) #x0000000000000000) (bvadd x x) x) x))) (ite (= (bvurem x #x0000000000000005) #x0000000000000000) (ite (= (bvsrem x #x000000000000000d) #x0000000000000000) x (ite (= (bvor #x0000000000000009 x) x) (bvadd x x) (ite (= (bvand #x0000000000000003 x) #x0000000000000001) (ite (= (bvashr x x) #x0000000000000000) x (bvadd x x)) x))) (ite (= (bvand #x0000000000000004 x) #x0000000000000000) (ite (= (bvsrem x #x0000000000000005) #x0000000000000000) (bvadd x x) (ite (= (bvurem x #x0000000000000003) #x0000000000000000) (ite (= (bvashr x x) #x0000000000000000) (ite (= (bvand #x0000000000000010 x) #x0000000000000000) (bvadd x x) x) (bvadd x x)) (ite (= (bvand #x0000000000000003 x) #x0000000000000001) (ite (= (bvsrem x #x0000000000000003) #x0000000000000000) (bvadd x x) (ite (= (bvsrem x #x0000000000000007) #x0000000000000000) (ite (= (bvand #x0000000000000010 x) #x0000000000000000) x (bvadd x x)) x)) x))) (ite (= (bvurem x #x0000000000000003) #x0000000000000000) (ite (= (bvand #x0000000000000003 x) #x0000000000000001) x (bvadd x x)) (bvadd x x)))))))
